Nuprl Lemma : Rinterface_wf
11,40
postcript
pdf
A
:Realizer. Rinterface(
A
)
Realizer
latex
Definitions
x
,
y
,
z
,
w
,
v
.
t
(
x
;
y
;
z
;
w
;
v
)
,
x
,
y
,
z
,
u
,
v
,
w
.
t
(
x
;
y
;
z
;
u
;
v
;
w
)
,
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
.
t
(
x
)
,
x
,
y
,
z
,
w
.
t
(
x
;
y
;
z
;
w
)
,
Rinterface(
A
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
x
(
s1
,
s2
,
s3
,
s4
,
s5
)
,
x
(
a
,
b
,
c
,
d
,
e
,
f
)
,
x
(
s1
,
s2
,
s3
)
,
x
(
s1
,
s2
,
s3
,
s4
)
Lemmas
finite-prob-space
wf
,
bool
wf
,
Rsends
wf
,
fpf
wf
,
decl-type
wf
,
decl-state
wf
,
Reffect
wf
,
isrcv
wf
,
IdLnk
wf
,
Knd
wf
,
Id
wf
,
rationals
wf
,
Rplus
wf
,
Rnone?
wf
,
ifthenelse
wf
,
let
wf
,
Rnone
wf
,
es
realizer
wf
,
es
realizer
ind
wf
origin
x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z. t(x;y;z), x. t(x), x,y,z,w. t(x;y;z;w), Rinterface(A), t 
T, 
x:A. B(x), x(s), x(s1,s2,s3,s4,s5), x(a,b,c,d,e,f), x(s1,s2,s3), x(s1,s2,s3,s4)